0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 89 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 10 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
maxC_in_gaa(s(T13), 0, s(T13)) → maxC_out_gaa(s(T13), 0, s(T13))
maxC_in_gaa(s(T23), s(T24), s(T23)) → U3_gaa(T23, T24, lessA_in_ag(T24, T23))
lessA_in_ag(0, s(T31)) → lessA_out_ag(0, s(T31))
lessA_in_ag(s(T38), s(T37)) → U1_ag(T38, T37, lessA_in_ag(T38, T37))
U1_ag(T38, T37, lessA_out_ag(T38, T37)) → lessA_out_ag(s(T38), s(T37))
U3_gaa(T23, T24, lessA_out_ag(T24, T23)) → maxC_out_gaa(s(T23), s(T24), s(T23))
maxC_in_gaa(0, T54, T54) → maxC_out_gaa(0, T54, T54)
maxC_in_gaa(s(T59), T61, T61) → U4_gaa(T59, T61, lessB_in_ga(T59, T61))
lessB_in_ga(0, s(T68)) → lessB_out_ga(0, s(T68))
lessB_in_ga(s(T73), s(T75)) → U2_ga(T73, T75, lessB_in_ga(T73, T75))
U2_ga(T73, T75, lessB_out_ga(T73, T75)) → lessB_out_ga(s(T73), s(T75))
U4_gaa(T59, T61, lessB_out_ga(T59, T61)) → maxC_out_gaa(s(T59), T61, T61)
maxC_in_gaa(s(T92), T94, T94) → U5_gaa(T92, T94, lessB_in_ga(T92, T94))
U5_gaa(T92, T94, lessB_out_ga(T92, T94)) → maxC_out_gaa(s(T92), T94, T94)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
maxC_in_gaa(s(T13), 0, s(T13)) → maxC_out_gaa(s(T13), 0, s(T13))
maxC_in_gaa(s(T23), s(T24), s(T23)) → U3_gaa(T23, T24, lessA_in_ag(T24, T23))
lessA_in_ag(0, s(T31)) → lessA_out_ag(0, s(T31))
lessA_in_ag(s(T38), s(T37)) → U1_ag(T38, T37, lessA_in_ag(T38, T37))
U1_ag(T38, T37, lessA_out_ag(T38, T37)) → lessA_out_ag(s(T38), s(T37))
U3_gaa(T23, T24, lessA_out_ag(T24, T23)) → maxC_out_gaa(s(T23), s(T24), s(T23))
maxC_in_gaa(0, T54, T54) → maxC_out_gaa(0, T54, T54)
maxC_in_gaa(s(T59), T61, T61) → U4_gaa(T59, T61, lessB_in_ga(T59, T61))
lessB_in_ga(0, s(T68)) → lessB_out_ga(0, s(T68))
lessB_in_ga(s(T73), s(T75)) → U2_ga(T73, T75, lessB_in_ga(T73, T75))
U2_ga(T73, T75, lessB_out_ga(T73, T75)) → lessB_out_ga(s(T73), s(T75))
U4_gaa(T59, T61, lessB_out_ga(T59, T61)) → maxC_out_gaa(s(T59), T61, T61)
maxC_in_gaa(s(T92), T94, T94) → U5_gaa(T92, T94, lessB_in_ga(T92, T94))
U5_gaa(T92, T94, lessB_out_ga(T92, T94)) → maxC_out_gaa(s(T92), T94, T94)
MAXC_IN_GAA(s(T23), s(T24), s(T23)) → U3_GAA(T23, T24, lessA_in_ag(T24, T23))
MAXC_IN_GAA(s(T23), s(T24), s(T23)) → LESSA_IN_AG(T24, T23)
LESSA_IN_AG(s(T38), s(T37)) → U1_AG(T38, T37, lessA_in_ag(T38, T37))
LESSA_IN_AG(s(T38), s(T37)) → LESSA_IN_AG(T38, T37)
MAXC_IN_GAA(s(T59), T61, T61) → U4_GAA(T59, T61, lessB_in_ga(T59, T61))
MAXC_IN_GAA(s(T59), T61, T61) → LESSB_IN_GA(T59, T61)
LESSB_IN_GA(s(T73), s(T75)) → U2_GA(T73, T75, lessB_in_ga(T73, T75))
LESSB_IN_GA(s(T73), s(T75)) → LESSB_IN_GA(T73, T75)
MAXC_IN_GAA(s(T92), T94, T94) → U5_GAA(T92, T94, lessB_in_ga(T92, T94))
maxC_in_gaa(s(T13), 0, s(T13)) → maxC_out_gaa(s(T13), 0, s(T13))
maxC_in_gaa(s(T23), s(T24), s(T23)) → U3_gaa(T23, T24, lessA_in_ag(T24, T23))
lessA_in_ag(0, s(T31)) → lessA_out_ag(0, s(T31))
lessA_in_ag(s(T38), s(T37)) → U1_ag(T38, T37, lessA_in_ag(T38, T37))
U1_ag(T38, T37, lessA_out_ag(T38, T37)) → lessA_out_ag(s(T38), s(T37))
U3_gaa(T23, T24, lessA_out_ag(T24, T23)) → maxC_out_gaa(s(T23), s(T24), s(T23))
maxC_in_gaa(0, T54, T54) → maxC_out_gaa(0, T54, T54)
maxC_in_gaa(s(T59), T61, T61) → U4_gaa(T59, T61, lessB_in_ga(T59, T61))
lessB_in_ga(0, s(T68)) → lessB_out_ga(0, s(T68))
lessB_in_ga(s(T73), s(T75)) → U2_ga(T73, T75, lessB_in_ga(T73, T75))
U2_ga(T73, T75, lessB_out_ga(T73, T75)) → lessB_out_ga(s(T73), s(T75))
U4_gaa(T59, T61, lessB_out_ga(T59, T61)) → maxC_out_gaa(s(T59), T61, T61)
maxC_in_gaa(s(T92), T94, T94) → U5_gaa(T92, T94, lessB_in_ga(T92, T94))
U5_gaa(T92, T94, lessB_out_ga(T92, T94)) → maxC_out_gaa(s(T92), T94, T94)
MAXC_IN_GAA(s(T23), s(T24), s(T23)) → U3_GAA(T23, T24, lessA_in_ag(T24, T23))
MAXC_IN_GAA(s(T23), s(T24), s(T23)) → LESSA_IN_AG(T24, T23)
LESSA_IN_AG(s(T38), s(T37)) → U1_AG(T38, T37, lessA_in_ag(T38, T37))
LESSA_IN_AG(s(T38), s(T37)) → LESSA_IN_AG(T38, T37)
MAXC_IN_GAA(s(T59), T61, T61) → U4_GAA(T59, T61, lessB_in_ga(T59, T61))
MAXC_IN_GAA(s(T59), T61, T61) → LESSB_IN_GA(T59, T61)
LESSB_IN_GA(s(T73), s(T75)) → U2_GA(T73, T75, lessB_in_ga(T73, T75))
LESSB_IN_GA(s(T73), s(T75)) → LESSB_IN_GA(T73, T75)
MAXC_IN_GAA(s(T92), T94, T94) → U5_GAA(T92, T94, lessB_in_ga(T92, T94))
maxC_in_gaa(s(T13), 0, s(T13)) → maxC_out_gaa(s(T13), 0, s(T13))
maxC_in_gaa(s(T23), s(T24), s(T23)) → U3_gaa(T23, T24, lessA_in_ag(T24, T23))
lessA_in_ag(0, s(T31)) → lessA_out_ag(0, s(T31))
lessA_in_ag(s(T38), s(T37)) → U1_ag(T38, T37, lessA_in_ag(T38, T37))
U1_ag(T38, T37, lessA_out_ag(T38, T37)) → lessA_out_ag(s(T38), s(T37))
U3_gaa(T23, T24, lessA_out_ag(T24, T23)) → maxC_out_gaa(s(T23), s(T24), s(T23))
maxC_in_gaa(0, T54, T54) → maxC_out_gaa(0, T54, T54)
maxC_in_gaa(s(T59), T61, T61) → U4_gaa(T59, T61, lessB_in_ga(T59, T61))
lessB_in_ga(0, s(T68)) → lessB_out_ga(0, s(T68))
lessB_in_ga(s(T73), s(T75)) → U2_ga(T73, T75, lessB_in_ga(T73, T75))
U2_ga(T73, T75, lessB_out_ga(T73, T75)) → lessB_out_ga(s(T73), s(T75))
U4_gaa(T59, T61, lessB_out_ga(T59, T61)) → maxC_out_gaa(s(T59), T61, T61)
maxC_in_gaa(s(T92), T94, T94) → U5_gaa(T92, T94, lessB_in_ga(T92, T94))
U5_gaa(T92, T94, lessB_out_ga(T92, T94)) → maxC_out_gaa(s(T92), T94, T94)
LESSB_IN_GA(s(T73), s(T75)) → LESSB_IN_GA(T73, T75)
maxC_in_gaa(s(T13), 0, s(T13)) → maxC_out_gaa(s(T13), 0, s(T13))
maxC_in_gaa(s(T23), s(T24), s(T23)) → U3_gaa(T23, T24, lessA_in_ag(T24, T23))
lessA_in_ag(0, s(T31)) → lessA_out_ag(0, s(T31))
lessA_in_ag(s(T38), s(T37)) → U1_ag(T38, T37, lessA_in_ag(T38, T37))
U1_ag(T38, T37, lessA_out_ag(T38, T37)) → lessA_out_ag(s(T38), s(T37))
U3_gaa(T23, T24, lessA_out_ag(T24, T23)) → maxC_out_gaa(s(T23), s(T24), s(T23))
maxC_in_gaa(0, T54, T54) → maxC_out_gaa(0, T54, T54)
maxC_in_gaa(s(T59), T61, T61) → U4_gaa(T59, T61, lessB_in_ga(T59, T61))
lessB_in_ga(0, s(T68)) → lessB_out_ga(0, s(T68))
lessB_in_ga(s(T73), s(T75)) → U2_ga(T73, T75, lessB_in_ga(T73, T75))
U2_ga(T73, T75, lessB_out_ga(T73, T75)) → lessB_out_ga(s(T73), s(T75))
U4_gaa(T59, T61, lessB_out_ga(T59, T61)) → maxC_out_gaa(s(T59), T61, T61)
maxC_in_gaa(s(T92), T94, T94) → U5_gaa(T92, T94, lessB_in_ga(T92, T94))
U5_gaa(T92, T94, lessB_out_ga(T92, T94)) → maxC_out_gaa(s(T92), T94, T94)
LESSB_IN_GA(s(T73), s(T75)) → LESSB_IN_GA(T73, T75)
LESSB_IN_GA(s(T73)) → LESSB_IN_GA(T73)
From the DPs we obtained the following set of size-change graphs:
LESSA_IN_AG(s(T38), s(T37)) → LESSA_IN_AG(T38, T37)
maxC_in_gaa(s(T13), 0, s(T13)) → maxC_out_gaa(s(T13), 0, s(T13))
maxC_in_gaa(s(T23), s(T24), s(T23)) → U3_gaa(T23, T24, lessA_in_ag(T24, T23))
lessA_in_ag(0, s(T31)) → lessA_out_ag(0, s(T31))
lessA_in_ag(s(T38), s(T37)) → U1_ag(T38, T37, lessA_in_ag(T38, T37))
U1_ag(T38, T37, lessA_out_ag(T38, T37)) → lessA_out_ag(s(T38), s(T37))
U3_gaa(T23, T24, lessA_out_ag(T24, T23)) → maxC_out_gaa(s(T23), s(T24), s(T23))
maxC_in_gaa(0, T54, T54) → maxC_out_gaa(0, T54, T54)
maxC_in_gaa(s(T59), T61, T61) → U4_gaa(T59, T61, lessB_in_ga(T59, T61))
lessB_in_ga(0, s(T68)) → lessB_out_ga(0, s(T68))
lessB_in_ga(s(T73), s(T75)) → U2_ga(T73, T75, lessB_in_ga(T73, T75))
U2_ga(T73, T75, lessB_out_ga(T73, T75)) → lessB_out_ga(s(T73), s(T75))
U4_gaa(T59, T61, lessB_out_ga(T59, T61)) → maxC_out_gaa(s(T59), T61, T61)
maxC_in_gaa(s(T92), T94, T94) → U5_gaa(T92, T94, lessB_in_ga(T92, T94))
U5_gaa(T92, T94, lessB_out_ga(T92, T94)) → maxC_out_gaa(s(T92), T94, T94)
LESSA_IN_AG(s(T38), s(T37)) → LESSA_IN_AG(T38, T37)
LESSA_IN_AG(s(T37)) → LESSA_IN_AG(T37)
From the DPs we obtained the following set of size-change graphs: